\begin{tabbing}
$\forall$\=$k$:Knd, $T$, $A$, $B$:Type, $l$:IdLnk, $x$, ${\it tg}$:Id, $f$:($A$$\rightarrow$$B$$\rightarrow$$T$), $c$:($A$$\rightarrow$$B$$\rightarrow\mathbb{B}$), ${\it es}$:ES.\+
\\[0ex]$k$\=(v:$B$) sends\+
\\[0ex]$f$($x$:$A$,v) on
\\[0ex]$l$ tagged with ${\it tg}$:$T$
\\[0ex]provided $c$($x$,v)
\-\-\\[0ex]$\Rightarrow$ ($\exists$\=$g$:\{$e$:E$\mid$ loc($e$) = source($l$) $\in$ Id \& kind($e$) = $k$ \& ($\uparrow$($c$(($x$ when $e$),val($e$))))\} $\rightarrow$E\+
\\[0ex]($\forall$$e$:\{$e$:E$\mid$ loc($e$) = source($l$) $\in$ Id \& kind($e$) = $k$ \& ($\uparrow$($c$(($x$ when $e$),val($e$))))\} .
\\[0ex](kind($g$($e$)) = rcv($l$,${\it tg}$) $\in$ Knd)
\\[0ex]c$\wedge$ \=(sender($g$($e$)) = $e$\+
\\[0ex]\& ($\forall$${\it e''}$:E. (kind(${\it e''}$) = rcv($l$,${\it tg}$) $\in$ Knd) $\Rightarrow$ (sender(${\it e''}$) = $e$) $\Rightarrow$ (${\it e''}$ = $g$($e$)))
\\[0ex]\& val($g$($e$)) = $f$(($x$ when $e$),val($e$)))))
\-\-
\end{tabbing}